Goto

Collaborating Authors

 scalable neural network verification


Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

Neural Information Processing Systems

Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advancements. However, GCP-CROWN currently relies on ${\it generic}$ cutting planes (cuts) generated from external mixed integer programming (MIP) solvers.


Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

Neural Information Processing Systems

Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advancements. However, GCP-CROWN currently relies on {\it generic} cutting planes ("cuts") generated from external mixed integer programming (MIP) solvers. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes {\it specific} to this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), that leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts.